package procilege.test.simplecase;

import static org.junit.Assert.assertTrue;

import org.junit.Before;
import org.junit.Test;

import procilege.impl.DefaultProcilegeModule;
import procilege.lang.PrivilegeFormAnalysis;
import procilege.test.TestZero;
import procilege.test.pal.AbstractPalTest;

import com.google.inject.Guice;
import com.google.inject.Inject;
import com.google.inject.Injector;

public class PaperLv2007asd extends AbstractPalTest  {

	@Test
	public void play() {

		// SCENARIO-1
		tell("" // 
				+ "let doc1 is TechDoc \n" // 
				+ "reader := (read + list)/TechDoc \n" //
				+ "manager := (reader + write + remove)/TechDoc \n" //
				+ "bob := reader \n" //
				+ "may := manager \n" //
				+ "phone := read + write + list \n" //
		);

		// SCENARIO-2
		tell("" //
				+ "session1 := bob * phone \n" //
				+ "session2 := may * phone \n" //
		);

		// SCENARIO-3
		tell(""//
				+ "readGuard := readGuard * [session1 *~ read/doc1] \n" //
		);
		
		dumpHistory(0, 100);
		
		assertTrue(pfa.available(pfa.privform(nn("readGuard"))));

		// SCENARIO-4
		tell(""//
				+ "doc1 := readable + writable \n"
				+ "writeGuard := writeGuard * [session2 *~ write/doc1] \n"
				+ "writableGuard := writableGuard * [doc1 *~ writable] \n"
				+ "interaction1 := writeGuard + writableGuard \n");
		
		dumpHistory(0, 150);
		
		assertTrue(pfa.available(pfa.privform(nn("interaction1"))));
	}
}
